M.ef(k,x,s,v,w) == E != (M.2.2.2.2).1(<k, x>)  w = E(s,v) 

latex

---

clarification:

M.ef(k,x,s,v,w)
== fpf-val(product-deq(Knd;Id;KindDeq;IdDeq);
== fpf-val(((M.2.2.2.2).1);
== fpf-val(<k, x>;
== fpf-val(kx,E.(w = E(s,v)  M.ds(x))) 

latex

Definitions	z != f(x)  P(a;z), product-deq(A;B;a;b), Knd, Id, KindDeq, IdDeq, t.1, t.2, <a, b>, s = t, x:AB(x), , M.ds(x), f(a)
FDL editor aliases	ma-ef